es:ES{i}, e:E, x:Id. e copies x  Prop{i'} 

latex

Definitions	t  T, True, x:A. B(x), loc(e), Id, b, Void, x:AB(x), P  Q, False, A, P  Q, s = t, x:AB(x), P & Q, P  Q, T, ES, vartype(i;x), Type, E, state after e\\x, state@i\\x, x:T>>a, Prop, e receives a, state when e\\x, f(a), es-init(es;e), x when e, i >> a, Atom$n, x:A. B(x), e copies x
Lemmas	es-atom wf, es-when wf, es-init wf, atom-free-es-vartype, es-state-when-without wf, not wf, es-rcv-atom wf, inheres wf, es-state-without wf, es-state-after-without wf, atom-free-es-state-without, es-E wf, es-vartype wf, squash wf, true wf, event system wf, es-loc-init, es-loc-pred, Id wf, es-loc wf